/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
package alloy.bool;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.StringTokenizer;

import org.apache.commons.collections.Bag;
import org.apache.commons.collections.bag.HashBag;

import alloy.util.Dbg;
import alloy.util.TmpFiles;
import alloy.util.ExtraBagFunctions;

/**
 * this class exists to support the getAstStencil function
 * @author rseater
 */
public class UcoreProofProcessor {
	
	/**
	 * a {@link Bag} of the hit counts of templates as observed the last time getAstStencil was run
	 * the templates are ints represented as strings
	 * the number of times a template is in the bag is the number of times it appears in the ast .stc stencil file written
	 */
	private static Bag _templateCounts;
	
	public static void initSingleton() {
		_templateCounts = new HashBag();
	}
	
	/**
	 * Am I in debug mode? (If so, I will print out extra messages along the way)
	 */
	private static boolean Debug = false;

	/**
	 * constructor
	 */
	public UcoreProofProcessor() {
		initSingleton();
	}

	/**
	 * @return a HashBag that counts the frequency of each template in the most recent .stc stencil file
	 */
	public static Bag getTemplateCounts() {
		if (_templateCounts == null)
			Dbg.warn("UcoreProofProcessor has not been properly initialized to provide hit count information.");
		return (HashBag)_templateCounts;
	}
	
	/**
	 * @param template
	 * @return how many times that template was instantiated in the most recently written .stc stenicl file
	 */
	public static int getTemplateCount(int template) {
		if (_templateCounts == null)
			Dbg.warn("UcoreProofProcessor has not been properly initialized to provide hit count information.");
		return _templateCounts.getCount(String.valueOf(template));
	}
	
	/**
	 * this is the main controller for the algorithm this class exists to support
	 * it writes a template of the set of literals in an unsat core
	 * @param corefileName basename from which we can deduce the names of the iteration files (e.g. clauses.cnf)
	 * @param templateInstantiationFile .ist file that gives the mapping from literals to templates and arguments
	 * that when passed to the template produce the subtree rooted at the node that produced that literal
	 * @param astStencilFile where the template will be written
	 */
	public void getAstStencil(File coreFile, File templateInstantiationFile, File astStencilFile) {
		//find the final iteration of the core finding process:
		Dbg.info("Computing finalIteration with base " + coreFile.getName());
		final File finalIteration = findLastIterationFile(coreFile);

		//get the literals out of that core:
		Dbg.info("Computing coreLiterals from " + finalIteration.getName());
		final File hitCountFile = TmpFiles.createHandleToATempFile("hitCounts");
		final Set coreLiterals = getCoreLiterals(finalIteration, hitCountFile);

		//write an AST stencil by looking up each of the core literals in the ist file
		Dbg.info("Computing astStencil from ist file " + templateInstantiationFile.getName());
		final HashMap astStencilData = interpretArgValueCombo(templateInstantiationFile, coreLiterals);

		//write the appropriate stencil:
		Dbg.info("Writing astStencil into " + astStencilFile.getName());
		writeAstStencil(astStencilData, astStencilFile);
	}//getAstStencil
	
	/**
	 * @param baseFile the {@link File} that we are working on, from whose name
	 *        we can deduce the names of the iteration files
	 * @return the name of the largest (last) iteration {@link File} containing the unsat core clauses,
	 * @assumes the iteration {@link File}s are numbered in order starting with 1
	 * @expects there to be an iteration {@link File} named basename_iteration_1
	 * @unexpected return the name of what should be the first iteration file
	 */
	protected File findLastIterationFile(final File baseFile) {
		//Our current guess at what the smallest non-existant iteration file is.
		//The largest existing iteration file is thus one less than that.
		int currentGuess = 1;
		//iteration files take the form "clauses.cnf_iteration_16"
		File f = TmpFiles.createHandleToATempFile(baseFile.getName() + "_iteration_" + String.valueOf(currentGuess));

		//Make sure that there is SOME iteration file, or else it's pointless to try to find the maximum one
		//(in that case, we just give up and return what should be the first iteration file)
		if(!f.exists()) {
			System.out.println("Could not find unsat core iteration file (" + f.getName() + ").");
			f = TmpFiles.createHandleToATempFile (baseFile.getName() + "_iteration_" + String.valueOf(currentGuess));
			return f;
			}
		
		//This loop finds the smallest currentGuess such that basename_iteration_currentguess does NOT exist
		// (which is one higher than the largest currentGuess for which basename_iteration_currentGuess DOES exist)
		while(f.exists()) {
			currentGuess++;
			f = TmpFiles.createHandleToATempFile(baseFile.getName() + "_iteration_" + String.valueOf(currentGuess));
		}
		
		//So, here we decrement currentGuess to find the largest one that DOES exist.
		f = TmpFiles.createHandleToATempFile(baseFile.getName() + "_iteration_" + String.valueOf(currentGuess - 1));
		Dbg.info("The final iteration file is " + f.getName());
		return f;
	}//findLastIterationFile

	/**
	 * @param coreLiterals the {@link Bag} of literals to be written to {@link File}
	 * @param hitCountFile the {@link File} where the counts will be written
	 * @effect writes to a file in the temp directory
	 */
	protected void writeHitCountFile(final Bag coreLiterals, final File hitCountFile, final File finalIterationFile) {
		Dbg.info("Writing hitCountFile into " + hitCountFile.getName());
		BufferedWriter buffWriter = null;
		try {
			final FileWriter fw = new FileWriter(hitCountFile);
			buffWriter = new BufferedWriter(fw);

			buffWriter.write("# literal/fequency pairs");
			buffWriter.newLine();
			buffWriter.write("# resulted from iteration file " + finalIterationFile.getName());
			buffWriter.newLine();
			buffWriter.write("# highest count = " + ExtraBagFunctions.highestCount(coreLiterals));
			buffWriter.newLine();
			for (Iterator i = coreLiterals.uniqueSet().iterator(); i.hasNext();) {
				final String literal = (String) i.next();
				buffWriter.write(literal + " " + String.valueOf(coreLiterals.getCount(literal)));
				buffWriter.newLine();
			}
		} catch (IOException e) {
			System.out.println("Error writing to hit count file (" + hitCountFile.getName() + ").");
		} finally {
			if (buffWriter != null) {
				try { buffWriter.close(); } catch (IOException e) { /* ignore */}
			}
		}
	}

	/**
	 * @param finalIterationFile the last iteration {@link File} produced by running zcore until a fixed point
	 * @param hitCountFile {@link File} where the literal frequence info is written
	 * @return the {@link Set} of literals used in the core {@link File}
	 * delegates work to countCoreLiterals and writeHitCountFile
	 */
	protected Set getCoreLiterals(final File finalIterationFile, final File hitCountFile) {
		final Bag coreLiterals = countCoreLiterals(finalIterationFile);
		//this file is never read, but is a useful record for humans:
		writeHitCountFile(coreLiterals, hitCountFile, finalIterationFile);
		//this is the field that is actually read:
		//_hitCounts = coreLiterals;
		return coreLiterals.uniqueSet();
	}

	/**
	 * @param finalIterationFile the {@link File} containing the unsat core clauses and literals
	 * @return the {@link Bag} of literals used in the core file, counting how often each literal appears
	 */
	protected Bag countCoreLiterals(final File finalIterationFile) {
		final Bag /* int */ coreLiterals = new HashBag();
		BufferedReader reader = null;
		try {
			reader = new BufferedReader(new FileReader(finalIterationFile));
			String line = reader.readLine();
			//throw away the first line, which contains information we don't care about
			line = reader.readLine();

			while (line != null) {
				final StringTokenizer st = new StringTokenizer(line);
				if (st.hasMoreTokens()) {
					final String firstToken = st.nextToken();
					if (!firstToken.equals("c") && !firstToken.equals("p")) {
					//if (firstToken != "c" && firstToken != "p") {
						//then this line contains literals
						coreLiterals.add(firstToken);//this is the first one
						while (st.hasMoreTokens()) {//these are the rest
							final String currentToken = st.nextToken();
							//lines are terminated by a 0, and no literals are named 0, so discard all 0's
							if (!currentToken.equals("0")) {
								coreLiterals.add(currentToken);
								//Dbg.info("adding token " + currentToken);
							} else {
								//else assert !st.hasMoreTokens();
								//Dbg.info("not adding token " + currentToken);
							}
						}
					} else {
						//Dbg.info("ignoring line beginning with token " + firstToken);
						//else do nothing; the line is non-empty but is not a list of literals (e.g. a comment)
					}
				}//else do nothing; the line was empty
				line = reader.readLine();
			}
		} catch (IOException e) {
			System.out.println("Error reading from core file (" + finalIterationFile.getName() + ").");
		} finally {
			if (reader != null) { try { reader.close(); } catch(IOException e) {} }
		}
		return coreLiterals;
	}//getCoreLiterals

	/**
	 * @algorithm The algorithm is basically as follows:
	 *  Look up each core literal in the .ist file to find its template and arg combo pair(s).
	 *  Build up a stencil by recording a mapping from that template to that arg combo.
	 * 
	 * @param templateInstantiationFile a file that tells us, for each literal,
	 *	what template produced that literals node in the ast and what arg
	 *	combo had to be passed to that template to produce it
	 * @param coreLiterals the set of literals used in the core
	 * @return a {@link Map} from templates (strings representing integers) to
	 * 	sets of arg combos (sets of integers)
	 * 	such that applying that template to any of those arg combos
	 * 	produces the node corresponding to a literal in the core
	 */
	protected HashMap interpretArgValueCombo(final File templateInstantiationFile, final Set coreLiterals) {
		HashMap/*(String representing an int) maps to (HashSets of ints)*/ astStencil = new HashMap();
		int maxTemplateId = 0;
		BufferedReader reader = null;
		try {
			reader = new BufferedReader(new FileReader(templateInstantiationFile));
			String line = reader.readLine();
			while (line != null) {
				if(Debug) {Dbg.info("line: " + line);}
				StringTokenizer st = new StringTokenizer(line);
				while (st.hasMoreTokens()) {
					//assert literal != null;
					final String literal = st.nextToken();
					if(Debug) {Dbg.info(" literal: " + literal);}
					//assert String.valueOf(literal) >= 0;
					if (Integer.parseInt(literal) != 0) {
						//the file is terminated by a line that just contains " 0"
						//every non-terminal line contains 3 integers, separated by spaced, the first of which is never 0

						//assert templateId != null;
						final String templateId = st.nextToken();
						if(Debug) {Dbg.info(" template: " + templateId);}
						//assert String.valueOf(templateId) > 0;

						//assert argument != null;
						final String argument = st.nextToken();
						if(Debug) {Dbg.info(" argument: " + argument);}
						//assert String.valueOf(argument) >= 0;

						//assert !st.hasMoreTokens();
						maxTemplateId = Math.max(Integer.parseInt(templateId), maxTemplateId);
						if (coreLiterals.contains(literal)) {
							//since the literal is in the core, we add that literal's argo combo to the stencil file
							//it is positioned in the array at index templateId

							if(Debug) {Dbg.info(" (IN)");}
							if (!astStencil.containsKey(templateId))
								astStencil.put(templateId, new HashSet());
							//assert !((HashSet)(astStencil.get(templateId))).contains(argument));
							((HashSet)(astStencil.get(templateId))).add(argument);
						} else {
							if(Debug) {Dbg.info(" (OUT)");}
							//do nothing
						}
					} else {
						if(Debug) {Dbg.info("(EOF)");}
						//do nothing;
						// the first token (literal) was "0"
						// meaning that the line has no more tokens and the file has no more lines
						// and thus these while loops will terminate on their own
					}
				}
				line = reader.readLine();
			}
		} catch (IOException e) {
			System.out.println(e.toString());
			System.out.println("Error reading from template instantiation file (" + templateInstantiationFile.getName() + ").");
		} finally {
			if (reader != null) { try { reader.close(); } catch(IOException e) {} }
		}
		return astStencil;
	}//interpretArgValueCombo

	/**
	 * @mutates astStencilFileName's contents by writing to it
	 * @mutates _templateCounts to record the number of times each template is instantiated
	 * @param coreLiterals the {@link Set} of literals used in the core
	 * @param astStencil the name of the {@link File} that the ast stencil will be written to
	 * @param astStencilFile the AST stencil {@link File} which will be written based on those literals
	 */
	protected void writeAstStencil(final Map astStencil, final File astStencilFile) {
		BufferedWriter buffWriter = null;
		try {
			final FileWriter fw = new FileWriter(astStencilFile);
			buffWriter = new BufferedWriter(fw);
			
			//For each template i (string representing an int) in the ast stencil map...
			for (Iterator i = astStencil.keySet().iterator() ; i.hasNext() ; ) {//int i = 0; i < astStencil.size(); i++) {
				String currentKey = (String)i.next();

				//...look at the set of arg combos (ints) it maps to.
				final HashSet currentSetOfArgCombos = (HashSet)astStencil.get(currentKey);
				if(Debug) {Dbg.info("template " + currentKey);}

				//If there are any...
				if (currentSetOfArgCombos != null) {
					final int size = currentSetOfArgCombos.size();
					if(Debug) {Dbg.info(" size " + size);}

					//...record that number...
					_templateCounts.add(currentKey, size);

					//...write a preparatory line...
					buffWriter.write(currentKey + " " + size);

					//assert currentSetOfArgCombos.size() >= 1;
					//if there are no arg combos passed to the template,
					// then the template shouldn't be here in the first place

					//...then iterate over them, writing the ast stencil file as we go.
					//a null entry means that the set is empty so we just skip it
					for (Iterator j = currentSetOfArgCombos.iterator(); j.hasNext();) {
						final String literal = (String)j.next();
						buffWriter.write(" " + literal);
						buffWriter.newLine();	
						if(Debug) {Dbg.info("  arg " + literal);}
					}
				} else {
					
				}
			}
			//Once done, terminate the ast stencil file with a " 0" line
			buffWriter.write(" 0");
		} catch (IOException e) {
			System.out.println("Error writing to ast stencil file (" + astStencilFile.getName() + ").");
		} finally {
			if (buffWriter != null) {
				try { buffWriter.close(); }
				catch(IOException e) { /* ignore */ }
			}
		}
	}//writeAstStencil
	
}//class UcoreProofProcessor
